FDL - Nuprl Definition : existse-ge

Nuprl Definition : existse-ge

0,22

e'.P(e') ==

e':E. e

e' & P(e')

clarification:

existse-ge(es;e;e'.P(e')) ==

e':es-E(es). es-le(es;e;e') & P(e')

Definitions x:A. B(x), E, P & Q, e e'

FDL editor aliases existse-ge

Definitions	x:A. B(x), E, P & Q, e e'
FDL editor aliases	existse-ge